H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.928 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule List

((group :: [Bool] -> [[Bool]]) :: [Bool] -> [[Bool]])

module List where

import qualified Maybe
import qualified Prelude

group :: Eq a => [a] -> [[a]]

group

groupBy (==)

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

_ []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

(\(ys,_) ->ys) vv10

(\(_,zs) ->zs) vv10

module Maybe where

import qualified List
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(_,zs)→zs

is transformed to

zs0 (_,zs) = zs

The following Lambda expression

\(ys,_)→ys

is transformed to

ys0 (ys,_) = ys

The following Lambda expression

\(_,zs)→zs

is transformed to

zs1 (_,zs) = zs

The following Lambda expression

\(ys,_)→ys

is transformed to

ys1 (ys,_) = ys

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule List

((group :: [Bool] -> [[Bool]]) :: [Bool] -> [[Bool]])

module List where

import qualified Maybe
import qualified Prelude

group :: Eq a => [a] -> [[a]]

group

groupBy (==)

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

_ []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

ys0 vv10

ys0

(ys,_)

zs0 vv10

zs0

(_,zs)

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

xs@(wu : wv)

is replaced by the following term

wu : wv

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((group :: [Bool] -> [[Bool]]) :: [Bool] -> [[Bool]])

module List where

import qualified Maybe
import qualified Prelude

group :: Eq a => [a] -> [[a]]

group

groupBy (==)

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

vw []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

ys0 vv10

ys0

(ys,vx)

zs0 vv10

zs0

(vy,zs)

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

span p [] = ([],[])

span p (wu : wv)

| p wu

= (wu : ys,zs)

| otherwise

= ([],wu : wv)

where

vu43 = span p wv

ys = ys1 vu43

ys1 (ys,wx) = ys

zs = zs1 vu43

zs1 (ww,zs) = zs

is transformed to

span p [] = span3 p []

span p (wu : wv) = span2 p (wu : wv)

span2 p (wu : wv) =

span1 p wu wv (p wu)

where

span0 p wu wv True = ([],wu : wv)

span1 p wu wv True = (wu : ys,zs)

span1 p wu wv False = span0 p wu wv otherwise

vu43 = span p wv

ys = ys1 vu43

ys1 (ys,wx) = ys

zs = zs1 vu43

zs1 (ww,zs) = zs

span3 p [] = ([],[])

span3 xv xw = span2 xv xw

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule List

((group :: [Bool] -> [[Bool]]) :: [Bool] -> [[Bool]])

module List where

import qualified Maybe
import qualified Prelude

group :: Eq a => [a] -> [[a]]

group

groupBy (==)

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

vw []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

ys0 vv10

ys0

(ys,vx)

zs0 vv10

zs0

(vy,zs)

module Maybe where

import qualified List
import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

(x : ys) : groupBy eq zs

where

vv10 = span (eq x) xs

ys = ys0 vv10

ys0 (ys,vx) = ys

zs = zs0 vv10

zs0 (vy,zs) = zs

are unpacked to the following functions on top level

groupByVv10 xx xy xz = span (xx xy) xz

groupByZs0 xx xy xz (vy,zs) = zs

groupByYs xx xy xz = groupByYs0 xx xy xz (groupByVv10 xx xy xz)

groupByYs0 xx xy xz (ys,vx) = ys

groupByZs xx xy xz = groupByZs0 xx xy xz (groupByVv10 xx xy xz)

The bindings of the following Let/Where expression

span1 p wu wv (p wu)

where

span0 p wu wv True = ([],wu : wv)

span1 p wu wv True = (wu : ys,zs)

span1 p wu wv False = span0 p wu wv otherwise

vu43 = span p wv

ys = ys1 vu43

ys1 (ys,wx) = ys

zs = zs1 vu43

zs1 (ww,zs) = zs

are unpacked to the following functions on top level

span2Ys1 yu yv (ys,wx) = ys

span2Ys yu yv = span2Ys1 yu yv (span2Vu43 yu yv)

span2Vu43 yu yv = span yu yv

span2Span0 yu yv p wu wv True = ([],wu : wv)

span2Span1 yu yv p wu wv True = (wu : span2Ys yu yv,span2Zs yu yv)

span2Span1 yu yv p wu wv False = span2Span0 yu yv p wu wv otherwise

span2Zs yu yv = span2Zs1 yu yv (span2Vu43 yu yv)

span2Zs1 yu yv (ww,zs) = zs

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

mainModule List

(group :: [Bool] -> [[Bool]])

module List where

import qualified Maybe
import qualified Prelude

group :: Eq a => [a] -> [[a]]

group

groupBy (==)

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy	vw []	=	[]
groupBy	eq (x : xs)	=	(x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs)

groupByVv10

xx xy xz

span (xx xy) xz

groupByYs

xx xy xz

groupByYs0 xx xy xz (groupByVv10 xx xy xz)

groupByYs0

xx xy xz (ys,vx)

groupByZs

xx xy xz

groupByZs0 xx xy xz (groupByVv10 xx xy xz)

groupByZs0

xx xy xz (vy,zs)

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="group",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="group yw3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="groupBy (==) yw3",fontsize=16,color="burlywood",shape="triangle"];172[label="yw3/yw30 : yw31",fontsize=10,color="white",style="solid",shape="box"];4 -> 172[label="",style="solid", color="burlywood", weight=9];
172 -> 5[label="",style="solid", color="burlywood", weight=3];
173[label="yw3/[]",fontsize=10,color="white",style="solid",shape="box"];4 -> 173[label="",style="solid", color="burlywood", weight=9];
173 -> 6[label="",style="solid", color="burlywood", weight=3];
5[label="groupBy (==) (yw30 : yw31)",fontsize=16,color="black",shape="box"];5 -> 7[label="",style="solid", color="black", weight=3];
6[label="groupBy (==) []",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="(yw30 : groupByYs (==) yw30 yw31) : groupBy (==) (groupByZs (==) yw30 yw31)",fontsize=16,color="green",shape="box"];7 -> 9[label="",style="dashed", color="green", weight=3];
7 -> 10[label="",style="dashed", color="green", weight=3];
8[label="[]",fontsize=16,color="green",shape="box"];9[label="groupByYs (==) yw30 yw31",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10 -> 4[label="",style="dashed", color="red", weight=0];
10[label="groupBy (==) (groupByZs (==) yw30 yw31)",fontsize=16,color="magenta"];10 -> 12[label="",style="dashed", color="magenta", weight=3];
11[label="groupByYs0 (==) yw30 yw31 (groupByVv10 (==) yw30 yw31)",fontsize=16,color="black",shape="box"];11 -> 13[label="",style="solid", color="black", weight=3];
12[label="groupByZs (==) yw30 yw31",fontsize=16,color="black",shape="box"];12 -> 14[label="",style="solid", color="black", weight=3];
13[label="groupByYs0 (==) yw30 yw31 (span ((==) yw30) yw31)",fontsize=16,color="burlywood",shape="box"];175[label="yw31/yw310 : yw311",fontsize=10,color="white",style="solid",shape="box"];13 -> 175[label="",style="solid", color="burlywood", weight=9];
175 -> 15[label="",style="solid", color="burlywood", weight=3];
176[label="yw31/[]",fontsize=10,color="white",style="solid",shape="box"];13 -> 176[label="",style="solid", color="burlywood", weight=9];
176 -> 16[label="",style="solid", color="burlywood", weight=3];
14[label="groupByZs0 (==) yw30 yw31 (groupByVv10 (==) yw30 yw31)",fontsize=16,color="black",shape="box"];14 -> 17[label="",style="solid", color="black", weight=3];
15[label="groupByYs0 (==) yw30 (yw310 : yw311) (span ((==) yw30) (yw310 : yw311))",fontsize=16,color="black",shape="box"];15 -> 18[label="",style="solid", color="black", weight=3];
16[label="groupByYs0 (==) yw30 [] (span ((==) yw30) [])",fontsize=16,color="black",shape="box"];16 -> 19[label="",style="solid", color="black", weight=3];
17[label="groupByZs0 (==) yw30 yw31 (span ((==) yw30) yw31)",fontsize=16,color="burlywood",shape="box"];177[label="yw31/yw310 : yw311",fontsize=10,color="white",style="solid",shape="box"];17 -> 177[label="",style="solid", color="burlywood", weight=9];
177 -> 20[label="",style="solid", color="burlywood", weight=3];
178[label="yw31/[]",fontsize=10,color="white",style="solid",shape="box"];17 -> 178[label="",style="solid", color="burlywood", weight=9];
178 -> 21[label="",style="solid", color="burlywood", weight=3];
18[label="groupByYs0 (==) yw30 (yw310 : yw311) (span2 ((==) yw30) (yw310 : yw311))",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="groupByYs0 (==) yw30 [] (span3 ((==) yw30) [])",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="groupByZs0 (==) yw30 (yw310 : yw311) (span ((==) yw30) (yw310 : yw311))",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="groupByZs0 (==) yw30 [] (span ((==) yw30) [])",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="groupByYs0 (==) yw30 (yw310 : yw311) (span2Span1 ((==) yw30) yw311 ((==) yw30) yw310 yw311 ((==) yw30 yw310))",fontsize=16,color="burlywood",shape="box"];179[label="yw30/False",fontsize=10,color="white",style="solid",shape="box"];22 -> 179[label="",style="solid", color="burlywood", weight=9];
179 -> 26[label="",style="solid", color="burlywood", weight=3];
180[label="yw30/True",fontsize=10,color="white",style="solid",shape="box"];22 -> 180[label="",style="solid", color="burlywood", weight=9];
180 -> 27[label="",style="solid", color="burlywood", weight=3];
23[label="groupByYs0 (==) yw30 [] ([],[])",fontsize=16,color="black",shape="box"];23 -> 28[label="",style="solid", color="black", weight=3];
24[label="groupByZs0 (==) yw30 (yw310 : yw311) (span2 ((==) yw30) (yw310 : yw311))",fontsize=16,color="black",shape="box"];24 -> 29[label="",style="solid", color="black", weight=3];
25[label="groupByZs0 (==) yw30 [] (span3 ((==) yw30) [])",fontsize=16,color="black",shape="box"];25 -> 30[label="",style="solid", color="black", weight=3];
26[label="groupByYs0 (==) False (yw310 : yw311) (span2Span1 ((==) False) yw311 ((==) False) yw310 yw311 ((==) False yw310))",fontsize=16,color="burlywood",shape="box"];181[label="yw310/False",fontsize=10,color="white",style="solid",shape="box"];26 -> 181[label="",style="solid", color="burlywood", weight=9];
181 -> 31[label="",style="solid", color="burlywood", weight=3];
182[label="yw310/True",fontsize=10,color="white",style="solid",shape="box"];26 -> 182[label="",style="solid", color="burlywood", weight=9];
182 -> 32[label="",style="solid", color="burlywood", weight=3];
27[label="groupByYs0 (==) True (yw310 : yw311) (span2Span1 ((==) True) yw311 ((==) True) yw310 yw311 ((==) True yw310))",fontsize=16,color="burlywood",shape="box"];183[label="yw310/False",fontsize=10,color="white",style="solid",shape="box"];27 -> 183[label="",style="solid", color="burlywood", weight=9];
183 -> 33[label="",style="solid", color="burlywood", weight=3];
184[label="yw310/True",fontsize=10,color="white",style="solid",shape="box"];27 -> 184[label="",style="solid", color="burlywood", weight=9];
184 -> 34[label="",style="solid", color="burlywood", weight=3];
28[label="[]",fontsize=16,color="green",shape="box"];29[label="groupByZs0 (==) yw30 (yw310 : yw311) (span2Span1 ((==) yw30) yw311 ((==) yw30) yw310 yw311 ((==) yw30 yw310))",fontsize=16,color="burlywood",shape="box"];185[label="yw30/False",fontsize=10,color="white",style="solid",shape="box"];29 -> 185[label="",style="solid", color="burlywood", weight=9];
185 -> 35[label="",style="solid", color="burlywood", weight=3];
186[label="yw30/True",fontsize=10,color="white",style="solid",shape="box"];29 -> 186[label="",style="solid", color="burlywood", weight=9];
186 -> 36[label="",style="solid", color="burlywood", weight=3];
30[label="groupByZs0 (==) yw30 [] ([],[])",fontsize=16,color="black",shape="box"];30 -> 37[label="",style="solid", color="black", weight=3];
31[label="groupByYs0 (==) False (False : yw311) (span2Span1 ((==) False) yw311 ((==) False) False yw311 ((==) False False))",fontsize=16,color="black",shape="box"];31 -> 38[label="",style="solid", color="black", weight=3];
32[label="groupByYs0 (==) False (True : yw311) (span2Span1 ((==) False) yw311 ((==) False) True yw311 ((==) False True))",fontsize=16,color="black",shape="box"];32 -> 39[label="",style="solid", color="black", weight=3];
33[label="groupByYs0 (==) True (False : yw311) (span2Span1 ((==) True) yw311 ((==) True) False yw311 ((==) True False))",fontsize=16,color="black",shape="box"];33 -> 40[label="",style="solid", color="black", weight=3];
34[label="groupByYs0 (==) True (True : yw311) (span2Span1 ((==) True) yw311 ((==) True) True yw311 ((==) True True))",fontsize=16,color="black",shape="box"];34 -> 41[label="",style="solid", color="black", weight=3];
35[label="groupByZs0 (==) False (yw310 : yw311) (span2Span1 ((==) False) yw311 ((==) False) yw310 yw311 ((==) False yw310))",fontsize=16,color="burlywood",shape="box"];187[label="yw310/False",fontsize=10,color="white",style="solid",shape="box"];35 -> 187[label="",style="solid", color="burlywood", weight=9];
187 -> 42[label="",style="solid", color="burlywood", weight=3];
188[label="yw310/True",fontsize=10,color="white",style="solid",shape="box"];35 -> 188[label="",style="solid", color="burlywood", weight=9];
188 -> 43[label="",style="solid", color="burlywood", weight=3];
36[label="groupByZs0 (==) True (yw310 : yw311) (span2Span1 ((==) True) yw311 ((==) True) yw310 yw311 ((==) True yw310))",fontsize=16,color="burlywood",shape="box"];189[label="yw310/False",fontsize=10,color="white",style="solid",shape="box"];36 -> 189[label="",style="solid", color="burlywood", weight=9];
189 -> 44[label="",style="solid", color="burlywood", weight=3];
190[label="yw310/True",fontsize=10,color="white",style="solid",shape="box"];36 -> 190[label="",style="solid", color="burlywood", weight=9];
190 -> 45[label="",style="solid", color="burlywood", weight=3];
37[label="[]",fontsize=16,color="green",shape="box"];38[label="groupByYs0 (==) False (False : yw311) (span2Span1 ((==) False) yw311 ((==) False) False yw311 True)",fontsize=16,color="black",shape="box"];38 -> 46[label="",style="solid", color="black", weight=3];
39[label="groupByYs0 (==) False (True : yw311) (span2Span1 ((==) False) yw311 ((==) False) True yw311 False)",fontsize=16,color="black",shape="box"];39 -> 47[label="",style="solid", color="black", weight=3];
40[label="groupByYs0 (==) True (False : yw311) (span2Span1 ((==) True) yw311 ((==) True) False yw311 False)",fontsize=16,color="black",shape="box"];40 -> 48[label="",style="solid", color="black", weight=3];
41[label="groupByYs0 (==) True (True : yw311) (span2Span1 ((==) True) yw311 ((==) True) True yw311 True)",fontsize=16,color="black",shape="box"];41 -> 49[label="",style="solid", color="black", weight=3];
42[label="groupByZs0 (==) False (False : yw311) (span2Span1 ((==) False) yw311 ((==) False) False yw311 ((==) False False))",fontsize=16,color="black",shape="box"];42 -> 50[label="",style="solid", color="black", weight=3];
43[label="groupByZs0 (==) False (True : yw311) (span2Span1 ((==) False) yw311 ((==) False) True yw311 ((==) False True))",fontsize=16,color="black",shape="box"];43 -> 51[label="",style="solid", color="black", weight=3];
44[label="groupByZs0 (==) True (False : yw311) (span2Span1 ((==) True) yw311 ((==) True) False yw311 ((==) True False))",fontsize=16,color="black",shape="box"];44 -> 52[label="",style="solid", color="black", weight=3];
45[label="groupByZs0 (==) True (True : yw311) (span2Span1 ((==) True) yw311 ((==) True) True yw311 ((==) True True))",fontsize=16,color="black",shape="box"];45 -> 53[label="",style="solid", color="black", weight=3];
46[label="groupByYs0 (==) False (False : yw311) (False : span2Ys ((==) False) yw311,span2Zs ((==) False) yw311)",fontsize=16,color="black",shape="box"];46 -> 54[label="",style="solid", color="black", weight=3];
47[label="groupByYs0 (==) False (True : yw311) (span2Span0 ((==) False) yw311 ((==) False) True yw311 otherwise)",fontsize=16,color="black",shape="box"];47 -> 55[label="",style="solid", color="black", weight=3];
48[label="groupByYs0 (==) True (False : yw311) (span2Span0 ((==) True) yw311 ((==) True) False yw311 otherwise)",fontsize=16,color="black",shape="box"];48 -> 56[label="",style="solid", color="black", weight=3];
49[label="groupByYs0 (==) True (True : yw311) (True : span2Ys ((==) True) yw311,span2Zs ((==) True) yw311)",fontsize=16,color="black",shape="box"];49 -> 57[label="",style="solid", color="black", weight=3];
50[label="groupByZs0 (==) False (False : yw311) (span2Span1 ((==) False) yw311 ((==) False) False yw311 True)",fontsize=16,color="black",shape="box"];50 -> 58[label="",style="solid", color="black", weight=3];
51[label="groupByZs0 (==) False (True : yw311) (span2Span1 ((==) False) yw311 ((==) False) True yw311 False)",fontsize=16,color="black",shape="box"];51 -> 59[label="",style="solid", color="black", weight=3];
52[label="groupByZs0 (==) True (False : yw311) (span2Span1 ((==) True) yw311 ((==) True) False yw311 False)",fontsize=16,color="black",shape="box"];52 -> 60[label="",style="solid", color="black", weight=3];
53[label="groupByZs0 (==) True (True : yw311) (span2Span1 ((==) True) yw311 ((==) True) True yw311 True)",fontsize=16,color="black",shape="box"];53 -> 61[label="",style="solid", color="black", weight=3];
54[label="False : span2Ys ((==) False) yw311",fontsize=16,color="green",shape="box"];54 -> 62[label="",style="dashed", color="green", weight=3];
55[label="groupByYs0 (==) False (True : yw311) (span2Span0 ((==) False) yw311 ((==) False) True yw311 True)",fontsize=16,color="black",shape="box"];55 -> 63[label="",style="solid", color="black", weight=3];
56[label="groupByYs0 (==) True (False : yw311) (span2Span0 ((==) True) yw311 ((==) True) False yw311 True)",fontsize=16,color="black",shape="box"];56 -> 64[label="",style="solid", color="black", weight=3];
57[label="True : span2Ys ((==) True) yw311",fontsize=16,color="green",shape="box"];57 -> 65[label="",style="dashed", color="green", weight=3];
58[label="groupByZs0 (==) False (False : yw311) (False : span2Ys ((==) False) yw311,span2Zs ((==) False) yw311)",fontsize=16,color="black",shape="box"];58 -> 66[label="",style="solid", color="black", weight=3];
59[label="groupByZs0 (==) False (True : yw311) (span2Span0 ((==) False) yw311 ((==) False) True yw311 otherwise)",fontsize=16,color="black",shape="box"];59 -> 67[label="",style="solid", color="black", weight=3];
60[label="groupByZs0 (==) True (False : yw311) (span2Span0 ((==) True) yw311 ((==) True) False yw311 otherwise)",fontsize=16,color="black",shape="box"];60 -> 68[label="",style="solid", color="black", weight=3];
61[label="groupByZs0 (==) True (True : yw311) (True : span2Ys ((==) True) yw311,span2Zs ((==) True) yw311)",fontsize=16,color="black",shape="box"];61 -> 69[label="",style="solid", color="black", weight=3];
62[label="span2Ys ((==) False) yw311",fontsize=16,color="black",shape="triangle"];62 -> 70[label="",style="solid", color="black", weight=3];
63[label="groupByYs0 (==) False (True : yw311) ([],True : yw311)",fontsize=16,color="black",shape="box"];63 -> 71[label="",style="solid", color="black", weight=3];
64[label="groupByYs0 (==) True (False : yw311) ([],False : yw311)",fontsize=16,color="black",shape="box"];64 -> 72[label="",style="solid", color="black", weight=3];
65[label="span2Ys ((==) True) yw311",fontsize=16,color="black",shape="triangle"];65 -> 73[label="",style="solid", color="black", weight=3];
66[label="span2Zs ((==) False) yw311",fontsize=16,color="black",shape="triangle"];66 -> 74[label="",style="solid", color="black", weight=3];
67[label="groupByZs0 (==) False (True : yw311) (span2Span0 ((==) False) yw311 ((==) False) True yw311 True)",fontsize=16,color="black",shape="box"];67 -> 75[label="",style="solid", color="black", weight=3];
68[label="groupByZs0 (==) True (False : yw311) (span2Span0 ((==) True) yw311 ((==) True) False yw311 True)",fontsize=16,color="black",shape="box"];68 -> 76[label="",style="solid", color="black", weight=3];
69[label="span2Zs ((==) True) yw311",fontsize=16,color="black",shape="triangle"];69 -> 77[label="",style="solid", color="black", weight=3];
70[label="span2Ys1 ((==) False) yw311 (span2Vu43 ((==) False) yw311)",fontsize=16,color="black",shape="box"];70 -> 78[label="",style="solid", color="black", weight=3];
71[label="[]",fontsize=16,color="green",shape="box"];72[label="[]",fontsize=16,color="green",shape="box"];73[label="span2Ys1 ((==) True) yw311 (span2Vu43 ((==) True) yw311)",fontsize=16,color="black",shape="box"];73 -> 79[label="",style="solid", color="black", weight=3];
74[label="span2Zs1 ((==) False) yw311 (span2Vu43 ((==) False) yw311)",fontsize=16,color="black",shape="box"];74 -> 80[label="",style="solid", color="black", weight=3];
75[label="groupByZs0 (==) False (True : yw311) ([],True : yw311)",fontsize=16,color="black",shape="box"];75 -> 81[label="",style="solid", color="black", weight=3];
76[label="groupByZs0 (==) True (False : yw311) ([],False : yw311)",fontsize=16,color="black",shape="box"];76 -> 82[label="",style="solid", color="black", weight=3];
77[label="span2Zs1 ((==) True) yw311 (span2Vu43 ((==) True) yw311)",fontsize=16,color="black",shape="box"];77 -> 83[label="",style="solid", color="black", weight=3];
78[label="span2Ys1 ((==) False) yw311 (span ((==) False) yw311)",fontsize=16,color="burlywood",shape="box"];191[label="yw311/yw3110 : yw3111",fontsize=10,color="white",style="solid",shape="box"];78 -> 191[label="",style="solid", color="burlywood", weight=9];
191 -> 84[label="",style="solid", color="burlywood", weight=3];
192[label="yw311/[]",fontsize=10,color="white",style="solid",shape="box"];78 -> 192[label="",style="solid", color="burlywood", weight=9];
192 -> 85[label="",style="solid", color="burlywood", weight=3];
79[label="span2Ys1 ((==) True) yw311 (span ((==) True) yw311)",fontsize=16,color="burlywood",shape="box"];193[label="yw311/yw3110 : yw3111",fontsize=10,color="white",style="solid",shape="box"];79 -> 193[label="",style="solid", color="burlywood", weight=9];
193 -> 86[label="",style="solid", color="burlywood", weight=3];
194[label="yw311/[]",fontsize=10,color="white",style="solid",shape="box"];79 -> 194[label="",style="solid", color="burlywood", weight=9];
194 -> 87[label="",style="solid", color="burlywood", weight=3];
80[label="span2Zs1 ((==) False) yw311 (span ((==) False) yw311)",fontsize=16,color="burlywood",shape="box"];195[label="yw311/yw3110 : yw3111",fontsize=10,color="white",style="solid",shape="box"];80 -> 195[label="",style="solid", color="burlywood", weight=9];
195 -> 88[label="",style="solid", color="burlywood", weight=3];
196[label="yw311/[]",fontsize=10,color="white",style="solid",shape="box"];80 -> 196[label="",style="solid", color="burlywood", weight=9];
196 -> 89[label="",style="solid", color="burlywood", weight=3];
81[label="True : yw311",fontsize=16,color="green",shape="box"];82[label="False : yw311",fontsize=16,color="green",shape="box"];83[label="span2Zs1 ((==) True) yw311 (span ((==) True) yw311)",fontsize=16,color="burlywood",shape="box"];197[label="yw311/yw3110 : yw3111",fontsize=10,color="white",style="solid",shape="box"];83 -> 197[label="",style="solid", color="burlywood", weight=9];
197 -> 90[label="",style="solid", color="burlywood", weight=3];
198[label="yw311/[]",fontsize=10,color="white",style="solid",shape="box"];83 -> 198[label="",style="solid", color="burlywood", weight=9];
198 -> 91[label="",style="solid", color="burlywood", weight=3];
84[label="span2Ys1 ((==) False) (yw3110 : yw3111) (span ((==) False) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];84 -> 92[label="",style="solid", color="black", weight=3];
85[label="span2Ys1 ((==) False) [] (span ((==) False) [])",fontsize=16,color="black",shape="box"];85 -> 93[label="",style="solid", color="black", weight=3];
86[label="span2Ys1 ((==) True) (yw3110 : yw3111) (span ((==) True) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];86 -> 94[label="",style="solid", color="black", weight=3];
87[label="span2Ys1 ((==) True) [] (span ((==) True) [])",fontsize=16,color="black",shape="box"];87 -> 95[label="",style="solid", color="black", weight=3];
88[label="span2Zs1 ((==) False) (yw3110 : yw3111) (span ((==) False) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];88 -> 96[label="",style="solid", color="black", weight=3];
89[label="span2Zs1 ((==) False) [] (span ((==) False) [])",fontsize=16,color="black",shape="box"];89 -> 97[label="",style="solid", color="black", weight=3];
90[label="span2Zs1 ((==) True) (yw3110 : yw3111) (span ((==) True) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];90 -> 98[label="",style="solid", color="black", weight=3];
91[label="span2Zs1 ((==) True) [] (span ((==) True) [])",fontsize=16,color="black",shape="box"];91 -> 99[label="",style="solid", color="black", weight=3];
92[label="span2Ys1 ((==) False) (yw3110 : yw3111) (span2 ((==) False) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];92 -> 100[label="",style="solid", color="black", weight=3];
93[label="span2Ys1 ((==) False) [] (span3 ((==) False) [])",fontsize=16,color="black",shape="box"];93 -> 101[label="",style="solid", color="black", weight=3];
94[label="span2Ys1 ((==) True) (yw3110 : yw3111) (span2 ((==) True) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];94 -> 102[label="",style="solid", color="black", weight=3];
95[label="span2Ys1 ((==) True) [] (span3 ((==) True) [])",fontsize=16,color="black",shape="box"];95 -> 103[label="",style="solid", color="black", weight=3];
96[label="span2Zs1 ((==) False) (yw3110 : yw3111) (span2 ((==) False) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];96 -> 104[label="",style="solid", color="black", weight=3];
97[label="span2Zs1 ((==) False) [] (span3 ((==) False) [])",fontsize=16,color="black",shape="box"];97 -> 105[label="",style="solid", color="black", weight=3];
98[label="span2Zs1 ((==) True) (yw3110 : yw3111) (span2 ((==) True) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];98 -> 106[label="",style="solid", color="black", weight=3];
99[label="span2Zs1 ((==) True) [] (span3 ((==) True) [])",fontsize=16,color="black",shape="box"];99 -> 107[label="",style="solid", color="black", weight=3];
100[label="span2Ys1 ((==) False) (yw3110 : yw3111) (span2Span1 ((==) False) yw3111 ((==) False) yw3110 yw3111 ((==) False yw3110))",fontsize=16,color="burlywood",shape="box"];199[label="yw3110/False",fontsize=10,color="white",style="solid",shape="box"];100 -> 199[label="",style="solid", color="burlywood", weight=9];
199 -> 108[label="",style="solid", color="burlywood", weight=3];
200[label="yw3110/True",fontsize=10,color="white",style="solid",shape="box"];100 -> 200[label="",style="solid", color="burlywood", weight=9];
200 -> 109[label="",style="solid", color="burlywood", weight=3];
101[label="span2Ys1 ((==) False) [] ([],[])",fontsize=16,color="black",shape="box"];101 -> 110[label="",style="solid", color="black", weight=3];
102[label="span2Ys1 ((==) True) (yw3110 : yw3111) (span2Span1 ((==) True) yw3111 ((==) True) yw3110 yw3111 ((==) True yw3110))",fontsize=16,color="burlywood",shape="box"];201[label="yw3110/False",fontsize=10,color="white",style="solid",shape="box"];102 -> 201[label="",style="solid", color="burlywood", weight=9];
201 -> 111[label="",style="solid", color="burlywood", weight=3];
202[label="yw3110/True",fontsize=10,color="white",style="solid",shape="box"];102 -> 202[label="",style="solid", color="burlywood", weight=9];
202 -> 112[label="",style="solid", color="burlywood", weight=3];
103[label="span2Ys1 ((==) True) [] ([],[])",fontsize=16,color="black",shape="box"];103 -> 113[label="",style="solid", color="black", weight=3];
104[label="span2Zs1 ((==) False) (yw3110 : yw3111) (span2Span1 ((==) False) yw3111 ((==) False) yw3110 yw3111 ((==) False yw3110))",fontsize=16,color="burlywood",shape="box"];203[label="yw3110/False",fontsize=10,color="white",style="solid",shape="box"];104 -> 203[label="",style="solid", color="burlywood", weight=9];
203 -> 114[label="",style="solid", color="burlywood", weight=3];
204[label="yw3110/True",fontsize=10,color="white",style="solid",shape="box"];104 -> 204[label="",style="solid", color="burlywood", weight=9];
204 -> 115[label="",style="solid", color="burlywood", weight=3];
105[label="span2Zs1 ((==) False) [] ([],[])",fontsize=16,color="black",shape="box"];105 -> 116[label="",style="solid", color="black", weight=3];
106[label="span2Zs1 ((==) True) (yw3110 : yw3111) (span2Span1 ((==) True) yw3111 ((==) True) yw3110 yw3111 ((==) True yw3110))",fontsize=16,color="burlywood",shape="box"];205[label="yw3110/False",fontsize=10,color="white",style="solid",shape="box"];106 -> 205[label="",style="solid", color="burlywood", weight=9];
205 -> 117[label="",style="solid", color="burlywood", weight=3];
206[label="yw3110/True",fontsize=10,color="white",style="solid",shape="box"];106 -> 206[label="",style="solid", color="burlywood", weight=9];
206 -> 118[label="",style="solid", color="burlywood", weight=3];
107[label="span2Zs1 ((==) True) [] ([],[])",fontsize=16,color="black",shape="box"];107 -> 119[label="",style="solid", color="black", weight=3];
108[label="span2Ys1 ((==) False) (False : yw3111) (span2Span1 ((==) False) yw3111 ((==) False) False yw3111 ((==) False False))",fontsize=16,color="black",shape="box"];108 -> 120[label="",style="solid", color="black", weight=3];
109[label="span2Ys1 ((==) False) (True : yw3111) (span2Span1 ((==) False) yw3111 ((==) False) True yw3111 ((==) False True))",fontsize=16,color="black",shape="box"];109 -> 121[label="",style="solid", color="black", weight=3];
110[label="[]",fontsize=16,color="green",shape="box"];111[label="span2Ys1 ((==) True) (False : yw3111) (span2Span1 ((==) True) yw3111 ((==) True) False yw3111 ((==) True False))",fontsize=16,color="black",shape="box"];111 -> 122[label="",style="solid", color="black", weight=3];
112[label="span2Ys1 ((==) True) (True : yw3111) (span2Span1 ((==) True) yw3111 ((==) True) True yw3111 ((==) True True))",fontsize=16,color="black",shape="box"];112 -> 123[label="",style="solid", color="black", weight=3];
113[label="[]",fontsize=16,color="green",shape="box"];114[label="span2Zs1 ((==) False) (False : yw3111) (span2Span1 ((==) False) yw3111 ((==) False) False yw3111 ((==) False False))",fontsize=16,color="black",shape="box"];114 -> 124[label="",style="solid", color="black", weight=3];
115[label="span2Zs1 ((==) False) (True : yw3111) (span2Span1 ((==) False) yw3111 ((==) False) True yw3111 ((==) False True))",fontsize=16,color="black",shape="box"];115 -> 125[label="",style="solid", color="black", weight=3];
116[label="[]",fontsize=16,color="green",shape="box"];117[label="span2Zs1 ((==) True) (False : yw3111) (span2Span1 ((==) True) yw3111 ((==) True) False yw3111 ((==) True False))",fontsize=16,color="black",shape="box"];117 -> 126[label="",style="solid", color="black", weight=3];
118[label="span2Zs1 ((==) True) (True : yw3111) (span2Span1 ((==) True) yw3111 ((==) True) True yw3111 ((==) True True))",fontsize=16,color="black",shape="box"];118 -> 127[label="",style="solid", color="black", weight=3];
119[label="[]",fontsize=16,color="green",shape="box"];120[label="span2Ys1 ((==) False) (False : yw3111) (span2Span1 ((==) False) yw3111 ((==) False) False yw3111 True)",fontsize=16,color="black",shape="box"];120 -> 128[label="",style="solid", color="black", weight=3];
121[label="span2Ys1 ((==) False) (True : yw3111) (span2Span1 ((==) False) yw3111 ((==) False) True yw3111 False)",fontsize=16,color="black",shape="box"];121 -> 129[label="",style="solid", color="black", weight=3];
122[label="span2Ys1 ((==) True) (False : yw3111) (span2Span1 ((==) True) yw3111 ((==) True) False yw3111 False)",fontsize=16,color="black",shape="box"];122 -> 130[label="",style="solid", color="black", weight=3];
123[label="span2Ys1 ((==) True) (True : yw3111) (span2Span1 ((==) True) yw3111 ((==) True) True yw3111 True)",fontsize=16,color="black",shape="box"];123 -> 131[label="",style="solid", color="black", weight=3];
124[label="span2Zs1 ((==) False) (False : yw3111) (span2Span1 ((==) False) yw3111 ((==) False) False yw3111 True)",fontsize=16,color="black",shape="box"];124 -> 132[label="",style="solid", color="black", weight=3];
125[label="span2Zs1 ((==) False) (True : yw3111) (span2Span1 ((==) False) yw3111 ((==) False) True yw3111 False)",fontsize=16,color="black",shape="box"];125 -> 133[label="",style="solid", color="black", weight=3];
126[label="span2Zs1 ((==) True) (False : yw3111) (span2Span1 ((==) True) yw3111 ((==) True) False yw3111 False)",fontsize=16,color="black",shape="box"];126 -> 134[label="",style="solid", color="black", weight=3];
127[label="span2Zs1 ((==) True) (True : yw3111) (span2Span1 ((==) True) yw3111 ((==) True) True yw3111 True)",fontsize=16,color="black",shape="box"];127 -> 135[label="",style="solid", color="black", weight=3];
128 -> 136[label="",style="dashed", color="red", weight=0];
128[label="span2Ys1 ((==) False) (False : yw3111) (False : span2Ys ((==) False) yw3111,span2Zs ((==) False) yw3111)",fontsize=16,color="magenta"];128 -> 137[label="",style="dashed", color="magenta", weight=3];
128 -> 138[label="",style="dashed", color="magenta", weight=3];
129[label="span2Ys1 ((==) False) (True : yw3111) (span2Span0 ((==) False) yw3111 ((==) False) True yw3111 otherwise)",fontsize=16,color="black",shape="box"];129 -> 139[label="",style="solid", color="black", weight=3];
130[label="span2Ys1 ((==) True) (False : yw3111) (span2Span0 ((==) True) yw3111 ((==) True) False yw3111 otherwise)",fontsize=16,color="black",shape="box"];130 -> 140[label="",style="solid", color="black", weight=3];
131 -> 141[label="",style="dashed", color="red", weight=0];
131[label="span2Ys1 ((==) True) (True : yw3111) (True : span2Ys ((==) True) yw3111,span2Zs ((==) True) yw3111)",fontsize=16,color="magenta"];131 -> 142[label="",style="dashed", color="magenta", weight=3];
131 -> 143[label="",style="dashed", color="magenta", weight=3];
132 -> 144[label="",style="dashed", color="red", weight=0];
132[label="span2Zs1 ((==) False) (False : yw3111) (False : span2Ys ((==) False) yw3111,span2Zs ((==) False) yw3111)",fontsize=16,color="magenta"];132 -> 145[label="",style="dashed", color="magenta", weight=3];
132 -> 146[label="",style="dashed", color="magenta", weight=3];
133[label="span2Zs1 ((==) False) (True : yw3111) (span2Span0 ((==) False) yw3111 ((==) False) True yw3111 otherwise)",fontsize=16,color="black",shape="box"];133 -> 147[label="",style="solid", color="black", weight=3];
134[label="span2Zs1 ((==) True) (False : yw3111) (span2Span0 ((==) True) yw3111 ((==) True) False yw3111 otherwise)",fontsize=16,color="black",shape="box"];134 -> 148[label="",style="solid", color="black", weight=3];
135 -> 149[label="",style="dashed", color="red", weight=0];
135[label="span2Zs1 ((==) True) (True : yw3111) (True : span2Ys ((==) True) yw3111,span2Zs ((==) True) yw3111)",fontsize=16,color="magenta"];135 -> 150[label="",style="dashed", color="magenta", weight=3];
135 -> 151[label="",style="dashed", color="magenta", weight=3];
137 -> 62[label="",style="dashed", color="red", weight=0];
137[label="span2Ys ((==) False) yw3111",fontsize=16,color="magenta"];137 -> 152[label="",style="dashed", color="magenta", weight=3];
138 -> 66[label="",style="dashed", color="red", weight=0];
138[label="span2Zs ((==) False) yw3111",fontsize=16,color="magenta"];138 -> 153[label="",style="dashed", color="magenta", weight=3];
136[label="span2Ys1 ((==) False) (False : yw3111) (False : yw5,yw4)",fontsize=16,color="black",shape="triangle"];136 -> 154[label="",style="solid", color="black", weight=3];
139[label="span2Ys1 ((==) False) (True : yw3111) (span2Span0 ((==) False) yw3111 ((==) False) True yw3111 True)",fontsize=16,color="black",shape="box"];139 -> 155[label="",style="solid", color="black", weight=3];
140[label="span2Ys1 ((==) True) (False : yw3111) (span2Span0 ((==) True) yw3111 ((==) True) False yw3111 True)",fontsize=16,color="black",shape="box"];140 -> 156[label="",style="solid", color="black", weight=3];
142 -> 69[label="",style="dashed", color="red", weight=0];
142[label="span2Zs ((==) True) yw3111",fontsize=16,color="magenta"];142 -> 157[label="",style="dashed", color="magenta", weight=3];
143 -> 65[label="",style="dashed", color="red", weight=0];
143[label="span2Ys ((==) True) yw3111",fontsize=16,color="magenta"];143 -> 158[label="",style="dashed", color="magenta", weight=3];
141[label="span2Ys1 ((==) True) (True : yw3111) (True : yw7,yw6)",fontsize=16,color="black",shape="triangle"];141 -> 159[label="",style="solid", color="black", weight=3];
145 -> 62[label="",style="dashed", color="red", weight=0];
145[label="span2Ys ((==) False) yw3111",fontsize=16,color="magenta"];145 -> 160[label="",style="dashed", color="magenta", weight=3];
146 -> 66[label="",style="dashed", color="red", weight=0];
146[label="span2Zs ((==) False) yw3111",fontsize=16,color="magenta"];146 -> 161[label="",style="dashed", color="magenta", weight=3];
144[label="span2Zs1 ((==) False) (False : yw3111) (False : yw9,yw8)",fontsize=16,color="black",shape="triangle"];144 -> 162[label="",style="solid", color="black", weight=3];
147[label="span2Zs1 ((==) False) (True : yw3111) (span2Span0 ((==) False) yw3111 ((==) False) True yw3111 True)",fontsize=16,color="black",shape="box"];147 -> 163[label="",style="solid", color="black", weight=3];
148[label="span2Zs1 ((==) True) (False : yw3111) (span2Span0 ((==) True) yw3111 ((==) True) False yw3111 True)",fontsize=16,color="black",shape="box"];148 -> 164[label="",style="solid", color="black", weight=3];
150 -> 69[label="",style="dashed", color="red", weight=0];
150[label="span2Zs ((==) True) yw3111",fontsize=16,color="magenta"];150 -> 165[label="",style="dashed", color="magenta", weight=3];
151 -> 65[label="",style="dashed", color="red", weight=0];
151[label="span2Ys ((==) True) yw3111",fontsize=16,color="magenta"];151 -> 166[label="",style="dashed", color="magenta", weight=3];
149[label="span2Zs1 ((==) True) (True : yw3111) (True : yw11,yw10)",fontsize=16,color="black",shape="triangle"];149 -> 167[label="",style="solid", color="black", weight=3];
152[label="yw3111",fontsize=16,color="green",shape="box"];153[label="yw3111",fontsize=16,color="green",shape="box"];154[label="False : yw5",fontsize=16,color="green",shape="box"];155[label="span2Ys1 ((==) False) (True : yw3111) ([],True : yw3111)",fontsize=16,color="black",shape="box"];155 -> 168[label="",style="solid", color="black", weight=3];
156[label="span2Ys1 ((==) True) (False : yw3111) ([],False : yw3111)",fontsize=16,color="black",shape="box"];156 -> 169[label="",style="solid", color="black", weight=3];
157[label="yw3111",fontsize=16,color="green",shape="box"];158[label="yw3111",fontsize=16,color="green",shape="box"];159[label="True : yw7",fontsize=16,color="green",shape="box"];160[label="yw3111",fontsize=16,color="green",shape="box"];161[label="yw3111",fontsize=16,color="green",shape="box"];162[label="yw8",fontsize=16,color="green",shape="box"];163[label="span2Zs1 ((==) False) (True : yw3111) ([],True : yw3111)",fontsize=16,color="black",shape="box"];163 -> 170[label="",style="solid", color="black", weight=3];
164[label="span2Zs1 ((==) True) (False : yw3111) ([],False : yw3111)",fontsize=16,color="black",shape="box"];164 -> 171[label="",style="solid", color="black", weight=3];
165[label="yw3111",fontsize=16,color="green",shape="box"];166[label="yw3111",fontsize=16,color="green",shape="box"];167[label="yw10",fontsize=16,color="green",shape="box"];168[label="[]",fontsize=16,color="green",shape="box"];169[label="[]",fontsize=16,color="green",shape="box"];170[label="True : yw3111",fontsize=16,color="green",shape="box"];171[label="False : yw3111",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs(:(True, yw3111)) → new_span2Ys(yw3111)
new_span2Ys(:(True, yw3111)) → new_span2Zs(yw3111)
new_span2Zs(:(True, yw3111)) → new_span2Zs(yw3111)
new_span2Ys(:(True, yw3111)) → new_span2Ys(yw3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_span2Ys(:(True, yw3111)) → new_span2Zs(yw3111)
The graph contains the following edges 1 > 1
new_span2Ys(:(True, yw3111)) → new_span2Ys(yw3111)
The graph contains the following edges 1 > 1
new_span2Zs(:(True, yw3111)) → new_span2Zs(yw3111)
The graph contains the following edges 1 > 1
new_span2Zs(:(True, yw3111)) → new_span2Ys(yw3111)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Ys0(:(False, yw3111)) → new_span2Zs0(yw3111)
new_span2Zs0(:(False, yw3111)) → new_span2Ys0(yw3111)
new_span2Ys0(:(False, yw3111)) → new_span2Ys0(yw3111)
new_span2Zs0(:(False, yw3111)) → new_span2Zs0(yw3111)

From the DPs we obtained the following set of size-change graphs:

new_span2Zs0(:(False, yw3111)) → new_span2Ys0(yw3111)
The graph contains the following edges 1 > 1
new_span2Zs0(:(False, yw3111)) → new_span2Zs0(yw3111)
The graph contains the following edges 1 > 1
new_span2Ys0(:(False, yw3111)) → new_span2Ys0(yw3111)
The graph contains the following edges 1 > 1
new_span2Ys0(:(False, yw3111)) → new_span2Zs0(yw3111)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_groupBy(:(yw30, yw31)) → new_groupBy(new_groupByZs0(yw30, yw31))

The TRS R consists of the following rules:

new_span2Ys2([]) → []
new_groupByZs0(True, :(True, yw311)) → new_span2Zs1(yw311)
new_span2Zs1([]) → []
new_span2Zs11(yw3111, yw11, yw10) → yw10
new_span2Ys2(:(True, yw3111)) → new_span2Ys10(yw3111, new_span2Ys2(yw3111), new_span2Zs1(yw3111))
new_span2Zs1(:(False, yw3111)) → :(False, yw3111)
new_span2Ys3([]) → []
new_span2Zs2([]) → []
new_groupByZs0(True, :(False, yw311)) → :(False, yw311)
new_span2Ys10(yw3111, yw7, yw6) → :(True, yw7)
new_groupByZs0(yw30, []) → []
new_span2Zs1(:(True, yw3111)) → new_span2Zs11(yw3111, new_span2Ys2(yw3111), new_span2Zs1(yw3111))
new_span2Ys2(:(False, yw3111)) → []
new_groupByZs0(False, :(True, yw311)) → :(True, yw311)
new_groupByZs0(False, :(False, yw311)) → new_span2Zs2(yw311)
new_span2Ys3(:(False, yw3111)) → new_span2Ys1(yw3111, new_span2Ys3(yw3111), new_span2Zs2(yw3111))
new_span2Zs2(:(False, yw3111)) → new_span2Zs10(yw3111, new_span2Ys3(yw3111), new_span2Zs2(yw3111))
new_span2Zs10(yw3111, yw9, yw8) → yw8
new_span2Ys1(yw3111, yw5, yw4) → :(False, yw5)
new_span2Zs2(:(True, yw3111)) → :(True, yw3111)
new_span2Ys3(:(True, yw3111)) → []

The set Q consists of the following terms:

new_groupByZs0(False, :(True, x0))
new_span2Ys2([])
new_span2Zs1([])
new_span2Ys3(:(True, x0))
new_span2Ys2(:(True, x0))
new_groupByZs0(False, :(False, x0))
new_span2Zs11(x0, x1, x2)
new_span2Zs2(:(True, x0))
new_span2Zs1(:(False, x0))
new_span2Ys10(x0, x1, x2)
new_span2Zs10(x0, x1, x2)
new_groupByZs0(x0, [])
new_span2Zs1(:(True, x0))
new_span2Zs2([])
new_span2Ys3([])
new_groupByZs0(True, :(False, x0))
new_groupByZs0(True, :(True, x0))
new_span2Zs2(:(False, x0))
new_span2Ys3(:(False, x0))
new_span2Ys2(:(False, x0))
new_span2Ys1(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_groupBy(:(yw30, yw31)) → new_groupBy(new_groupByZs0(yw30, yw31))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₂
POL(False) = 0
POL(True) = 0
POL([]) = 0
POL(new_groupBy(x₁)) = x₁
POL(new_groupByZs0(x₁, x₂)) = x₂
POL(new_span2Ys1(x₁, x₂, x₃)) = 1 + x₂
POL(new_span2Ys10(x₁, x₂, x₃)) = 1 + x₂
POL(new_span2Ys2(x₁)) = 1 + x₁
POL(new_span2Ys3(x₁)) = x₁
POL(new_span2Zs1(x₁)) = x₁
POL(new_span2Zs10(x₁, x₂, x₃)) = 1 + x₃
POL(new_span2Zs11(x₁, x₂, x₃)) = x₃
POL(new_span2Zs2(x₁)) = x₁

The following usable rules [17] were oriented:

new_span2Zs1(:(False, yw3111)) → :(False, yw3111)
new_groupByZs0(True, :(True, yw311)) → new_span2Zs1(yw311)
new_span2Ys1(yw3111, yw5, yw4) → :(False, yw5)
new_span2Ys3(:(False, yw3111)) → new_span2Ys1(yw3111, new_span2Ys3(yw3111), new_span2Zs2(yw3111))
new_span2Zs2(:(True, yw3111)) → :(True, yw3111)
new_span2Ys3([]) → []
new_span2Zs1([]) → []
new_groupByZs0(False, :(False, yw311)) → new_span2Zs2(yw311)
new_span2Zs1(:(True, yw3111)) → new_span2Zs11(yw3111, new_span2Ys2(yw3111), new_span2Zs1(yw3111))
new_span2Zs11(yw3111, yw11, yw10) → yw10
new_span2Zs2([]) → []
new_groupByZs0(False, :(True, yw311)) → :(True, yw311)
new_span2Ys3(:(True, yw3111)) → []
new_groupByZs0(yw30, []) → []
new_span2Ys2([]) → []
new_span2Ys2(:(True, yw3111)) → new_span2Ys10(yw3111, new_span2Ys2(yw3111), new_span2Zs1(yw3111))
new_groupByZs0(True, :(False, yw311)) → :(False, yw311)
new_span2Ys2(:(False, yw3111)) → []
new_span2Zs10(yw3111, yw9, yw8) → yw8
new_span2Zs2(:(False, yw3111)) → new_span2Zs10(yw3111, new_span2Ys3(yw3111), new_span2Zs2(yw3111))
new_span2Ys10(yw3111, yw7, yw6) → :(True, yw7)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_span2Ys2([]) → []
new_groupByZs0(True, :(True, yw311)) → new_span2Zs1(yw311)
new_span2Zs1([]) → []
new_span2Zs11(yw3111, yw11, yw10) → yw10
new_span2Ys2(:(True, yw3111)) → new_span2Ys10(yw3111, new_span2Ys2(yw3111), new_span2Zs1(yw3111))
new_span2Zs1(:(False, yw3111)) → :(False, yw3111)
new_span2Ys3([]) → []
new_span2Zs2([]) → []
new_groupByZs0(True, :(False, yw311)) → :(False, yw311)
new_span2Ys10(yw3111, yw7, yw6) → :(True, yw7)
new_groupByZs0(yw30, []) → []
new_span2Zs1(:(True, yw3111)) → new_span2Zs11(yw3111, new_span2Ys2(yw3111), new_span2Zs1(yw3111))
new_span2Ys2(:(False, yw3111)) → []
new_groupByZs0(False, :(True, yw311)) → :(True, yw311)
new_groupByZs0(False, :(False, yw311)) → new_span2Zs2(yw311)
new_span2Ys3(:(False, yw3111)) → new_span2Ys1(yw3111, new_span2Ys3(yw3111), new_span2Zs2(yw3111))
new_span2Zs2(:(False, yw3111)) → new_span2Zs10(yw3111, new_span2Ys3(yw3111), new_span2Zs2(yw3111))
new_span2Zs10(yw3111, yw9, yw8) → yw8
new_span2Ys1(yw3111, yw5, yw4) → :(False, yw5)
new_span2Zs2(:(True, yw3111)) → :(True, yw3111)
new_span2Ys3(:(True, yw3111)) → []

The set Q consists of the following terms:

new_groupByZs0(False, :(True, x0))
new_span2Ys2([])
new_span2Zs1([])
new_span2Ys3(:(True, x0))
new_span2Ys2(:(True, x0))
new_groupByZs0(False, :(False, x0))
new_span2Zs11(x0, x1, x2)
new_span2Zs2(:(True, x0))
new_span2Zs1(:(False, x0))
new_span2Ys10(x0, x1, x2)
new_span2Zs10(x0, x1, x2)
new_groupByZs0(x0, [])
new_span2Zs1(:(True, x0))
new_span2Zs2([])
new_span2Ys3([])
new_groupByZs0(True, :(False, x0))
new_groupByZs0(True, :(True, x0))
new_span2Zs2(:(False, x0))
new_span2Ys3(:(False, x0))
new_span2Ys2(:(False, x0))
new_span2Ys1(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

span2Span1	yu yv p wu wv True	= (wu : span2Ys yu yv,span2Zs yu yv)
span2Span1	yu yv p wu wv False	= span2Span0 yu yv p wu wv otherwise